perm filename MINKER[E83,JMC] blob
sn#722123 filedate 1983-08-02 generic text, type T, neo UTF8
∂28-Jul-83 1557 minker.umcp-cs@UDel-Relay Non-Monotonic Logic
Received: from UDEL-RELAY by SU-AI with TCP/SMTP; 28 Jul 83 15:56:07 PDT
Date: 28 Jul 83 16:09:17 EDT (Thu)
From: JACK MINKER <minker.umcp-cs@UDel-Relay>
Return-Path: <minker.umcp-cs@UDel-Relay>
Subject: Non-Monotonic Logic
To: "uw-beaver!ubc-vision!Reiter"@LBL-UNIX, Moore@SRI-AI, Mcdermott@YALE,
JMC@SU-AI
Via: UMCP-CS; 28 Jul 83 18:15-EDT
Below is a PRELIMINARY DRAFT of a paper thar Don Perlis and I
are writing. The paper is not yet completed. We are sending you the DRAFT
since it is relevant to our panel session at IJCAI. We would welcome any
comments that you may have on the material. Ilook forward to our panel session.
(D R A F T)
On the Semantics of Circumscription
J. Minker and D. Perlis
Computer Science Department
University of Maryland
College Park, MD 20742
July 1983
I. Introduction
We investigate the model theory of the notion of
circumscription (McCarthy [1980]), and find a completeness theorem that
provides both a generalization and its converse, to a result of
McCarthy. In particular, we extend the idea of circumscription to
allow prescription of what objects are or are not to be included in the
circumscription process, broadening the applicability of the technique.
Then we show that the circumscriptive theorems are precisely the truths
of the minimal models, in the case of 'finitary' theories.
As an example, consider the following problem: Someone asks
you whether you have ever known the phone number of a movie star. You
pause only a split second before answering 'No.' Later, on being asked
whether you have ever known the phone number of your uncle in
Chattanooga, you hesitate, frown, and end up saying that you are not
sure.
We apparently circumscribe on a movie star's number, but not on
an uncle's. That is, if our data base does not contain the fact that
we have ever known a star's number, we conclude we have not ever so
known; but we are not so hasty in other cases. Some things we realize
may well be true (we may have once known Uncle's number after all) even
if we cannot get our hands on them. So we would like a kind of
built-in 'protection' for the uncertainty of certain things while still
circumscribing over others. Indeed, it would seem that this is the
more common condition, for rarely outside of artificial problems like
the missionary-cannibal one of McCarthy, is it wise to assume we know
all that is relevant about a given matter. Of course, as McCarthy
points out, circumscription may be useful for a first pass at a problem
and later discarded or revised. But at some point the kind of
protected circumscription we urge here becomes relevant.
As a further motivation, suppose a database DB is given, and
that as is usual the queries Q that are answerable affirmatively are
the ones that are true with respect to an intended real-world model,
with the exception of certain queries regarding items that we know have
not been specified completely yet in DB. E.g., we may know data is
still being gathered on these items, such as, say, incomes of
middle-level management in a large company, while all the other entries
in DB may be complete. We may wish to reason about DB assuming that all
data is known (closed world assumption) except for these incomes.
II. The idea of circumscription
We review briefly the idea of circumscription. Given a
predicate symbol P and a formula A[P] containing P, the circumscription
of P by A[P] can be thought of as saying that the P-things consist of
certain ones as needed to satisfy A[P] and no more, in the sense that
any P-things Z satisfying A[Z] already include ALL P-things:
P
C [Z]: [A[Z] & (x)(Z(x)-->P(x))] --> (x)(P(x) --> Z(x)),
A
or alternatively
[A[Z] & (x)(Z(x)-->P(x))] --> (x)(-Z(x) --> -P(x)),
which emphasizes the use of circumscription to prove something is NOT a
P-thing.
Reiter, in unpublished work, has shown that the following
schema is equivalent to McCarthy's:
[A[P&Z] --> (x)(P(x)-->Z(x)),
which can be interpreted intuitively as saying that any strengthening
of P, such as P&Z, which conforms to the axioms A under consideration
for defining P, is no real strengthening: P already entails Z. This
is a very satisfying form for it incorporates the puzzling second
antecedent of McCarthy's schema in a natural version of the first.
A key example, emphasized by McCarthy, is the following: let
A[P] be P(a) v P(b). Let Z1(x) be x=a and Z2(x) be x=b. Then from
P(a) v P(b) we get that either Z1 or Z2 can serve for circumscription,
i.e., either P(x) --> Z1(x) or P(x) --> Z2(x). Thus either a is the
only P-thing, or b is: (E!x)(P(x) & (y)(y=/=x --> -P(y)). We will use
this idea later.
We point out the following lemma, that is instructive and is
related to later results:
Lemma 1: Let A[P] be -P(a) v Q. Then -P(a) is a result of
circumscription of P by A[P]. So -P(a) v Q is redundant,
since -P(a) is already a result of circumscription from the
empty set.
Proof: Let Z(x) be x=/=a & P(x). Then it is easy to see that A[Z]
holds. Furthermore, Z(x) --> P(x) trivially. Thus by
circumscription we have P(x) --> Z(x) and so we get P(x) -->
x=/=a, i.e., -P(a). <>
Note that in Reiter's form mentioned above, this is especially
suggestive, in that we simply let Z(x) be x=/=a and check that A[P&Z]
holds.
Now, an obvious reply to the above problem is that if we are
thinking of circumscribing the predicate symbol P in an axiom A, except
that we wish to protect the uncertainty of certain items, say those
with property S, then we should really be circumscribing the predicate
P(x) & -S(x), and then simply follow McCarthy. However, McCarthy's
technique requires that a single predicate symbol be used, not a
non-atomic formula. If we try to accomodate to this by introducing a
new symbol, say Q, with the additional axiom Q(x) <--> P(x) & -S(x),
then we will have immediate difficulties, since it is no longer clear
what axioms A to circumscribe Q in: if we include the defining formula
for Q then any circumscribing predicate substitution Z for Q simply
leads to the need to prove what we want to conclude, i.e., Z <--> Q.
And if we leave it out, then we have nothing to work on. Now of course
we can carefully analyze whatever axioms A had already been chosen for
circumscribing P in the first place, and re-tailor them for the new
situation protecting S. But this is more work, and it is not clear
what a general method for this would be.
III. Circumscription with protected terms
Here we show that a simple syntactic device will yield the
desired result in such cases. We suggest that once A has been selected
as appropriate for circumscribing P, and if (perhaps later) it is
desired to protect S-things from this process so that circumscription
will not be used to show S-things are not P-things, we can keep the
same criteria A, but alter the form of the schema itself. Starting
with P(x) & -S(x) as above, which we write P/S(x) (and more generally
T/U(x) for T(x) & -U(x)), we alter the circumscription schema to read
as follows:
P/S
C [Z]: [A[Z] & (x)(Z/S(x)-->P(x))] --> (x)(-Z/S(x) --> -P(x))
A
for all predicate symbols Z. (Here -Z/S means (-Z)/S and not -(Z/S).)
Intuitively, we are saying that conclusions are drawn only about
non-S-things, as far as ruling out possible P-things goes. Notice that
the conclusion is equivalent to (x)(P/S(x) --> Z(x)). We refer to this
schema as protected circumscription; unless so indicated,
circumscription will refer to McCarthy's schema. We write C[Z] when
context makes clear what the A, P, and S (if protected) are.
We consider some examples. Suppose HKP(x) says, "have known
the phone number of x." We would like to stipulate as a first
approximation that if we cannot determine that we have known x's phone
number, then in fact we have not so known. This might be accomplished
by stating that HKP is circumscribed by the formula A[HKP]:
HKP(a)&HKP(b)&HKP(c)&...&HKP(n) where a,b,...,n are particular
individuals whose numbers we do recall having known. Now suppose we
want to alter this so that it applies only to famous people (F(x)) or
lovers (L(x))--not uncles, etc. That is, we expect to recall if we
have ever known the number of a movie star just as we would recall if
we have not learned the number of our lover, but in other cases we are
often unsure. We then set up the protected circumpscription schema:
[A[Z] & (x)(Z/S(x)-->HKP(x)] --> (x)(-Z/S(x) --> -HKP(x))
where S(x) <--> -F(x) & -L(x).
Consider how this works now for a movie star s. Assume in fact
that HKP(s) is not in our database. Then we circumscribe on the
predicate Z(x): (x = a)v(x = b)v...v(x = n). Since A[Z] is easily
verified in the database, and since in this case in fact Z(x) -->
HKP(x), we obtain (x)(-Z/S(x) --> -HKP(x). Hence, instantiating s and
assuming F(s) to be in the database, we end up with -Z(s) --> -HKP(s).
But since -Z(s) (recall s is not any of a,...,n), we conclude that we
have never known s's phone number. (Admittedly this is not the
split-second reasoning of our opening motivational
statement--circumscription seems to share, with other non-monotonic
modes of inference, a rather substantial computational burden.
However, we will see later that in a precise sense the only instances
of Z that are of significance are those as above: disjunctions of the
form x=a v ... v x=n, providing a guide of sorts to the calculations.
Consider a variation on this. Suppose we recall having once
known the phone number of a movie star, but cannot recall who. Thus
(Ex)(HKP(x)&F(x)). We circumscribe HKP by this formula as well as the
above HKP(a)&...&HKP(n), i.e., A is now the conjunction of these two
formulas. Again, we want to protect those who are not famous or
lovers, so that we will not conclude we have not known x's phone number
merely because we cannot recall so, if x is not 'noteworthy'. Let s be
a Skolem constant for (Ex)(HKP(x) & F(x)). This time, we use for Z(x)
the formula (x = s)v(x = a)v...v(x = n). Then A[Z] holds, for
it is
(Ex)((x=s) v (x=a) v ... v (x=n) & F(x))
&
(a=y) v (a=a) v ... v (a=n)
&
.
.
.
&
(n=y) v (n=a) v ... v (n=n)
where we know x=s satisfies the first conjunct, and the rest are
tautologies.
Now we know HKP(s)&F(s); from this we can conclude (x)(Z/S(x)-->HKP(x))
since the latter really amounts to the conjunction of
F(s)vL(s) --> HKP(s)
F(a)vL(a) --> HKP(a)
.
.
.
F(n)vL(n) --> HKP(n)
where we already know all the right-hand sides. Then by protected
circumscription we get (x)(-Z/S(x) --> -HKP(x)). We existentially
quantify this, to get
(Ey)(x)([x=/=y & x=/=a &...& x=/=n & (F(x)vL(x))] --> -HKP(x)),
ie, we have known the phone number of at most one famous person or
lover different from a,...,n, and in particular then of at most one
famous person different from a,...,n.
IV. Models
We must re-define minimal model in an manner appropriate to the
new version of circumscription. Let M and N be models of A[P]. We say
M <P/S N if the atomic truths of M are contained in those of N, if
those atomic truths of M not using P are precisely those of N, and if
the extension of P&S in M is also that in N. Then M is a P/S-minimal
model of A[P] if M is a model of A[P] minimal with respect to the
relation <P/S.
As an example, suppose P(a)&P(b)&P(c)&-P(d)&Q(d) is the
sentence A[P], and we wish to protect the constant c: S(c). Then the
only model is {P(a) P(b) P(c) Q(d) S(c)}. (Here we indicate a model by
writing the positive ground clauses that hold in it.) This model is
the only minimal model. In this case protection is superfluous since
P(c) is required to hold.
Now consider the sentence P(a)&P(b) where c is still a
protected constant--S(c)--and d is an unprotected constant. Here we
obtain four models:
M1={P(a) P(b) P(c) P(d) S(c)}
M2={P(a) P(b) P(c) S(c)}
M3={P(a) P(b) P(d) S(c)}
M4={P(a) P(b) S(c)}.
Of these only M2 and M4 are minimal, M2 being a P/S-minimal submodel of
M1, and M4 of M3.
Finally, consider P(a) v P(b) v P(c) with S(a) and S(c). Then
the models are
M1={P(a) P(b) P(c) S(a) S(c)}
M2={P(a) P(b) S(a) S(c)}
M3={P(a) P(c) S(a) S(c)}
M4={P(b) P(c) S(a) S(c)}
M5={P(a) S(a) S(c)}
M6={P(b) S(a) S(c)}
M7={P(c) S(a) S(c)}.
The minimal ones are M3, M5, M6, M7.
V. Completeness results
McCarthy [1980] provides the soundness half of a model theory
for circumscription, but not the completeness part. As noted by Davis
[1980] (see below) the fully general completeness result would be
false. Nonetheless, Minker [1982] has a soundness and completeness
result for the highly analogous situation of generalized closed world
assumptions. Here we look for a parallel to Minker's work in
restricted cases, and obtain both soundness and completeness there for
circumscription and protected circumscription.
We begin by demonstrating that our schema C[Z] does provide an
extension of McCarthy's circumpscription for protected terms. First,
we prove the following lemma:
Lemma 2: A[P] |P/S== C[Z], where the P/S-double-turnstile means the
consequent holds in any P/S-minimal model of the antecedent,
and Z and S are any formulas not involving P. (When we intend
ordinary circumscription we will write A[P] |c== B to mean B
holds in any minimal model of A[P], and A[P] |c-- B to mean B
is a circumscriptive theorem of A[P].)
Proof: We follow McCarthy, giving further details to make clear where
there is a difference with our approach.
Let Z be a formula not involving P. Then we must show that the
schema C[Z] holds in an arbitrary P/S-minimal model M. So
assume A[Z] & (x)(Z/S(x) --> P(x)) holds in M but (x)(-Z/S(x)
--> -P(x)) fails in M. Define M' to be the submodel of M where
all atomic formulas P(x) for which -Z/S(x) holds in M are
removed.
We wish to show M' is a model for A[P], contradicting M being a
P/S-minimal model for A[P]. For clearly M' <P/S M, and M' =/=
M. But A[Z] holds in M, so that it also holds in M'. Thus any
logical consequences of A[Z] also hold in M'. Now if A[P]
fails in M' then some consequence P(a)v...vP(n) must fail,
whereas Z(a)v...vZ(n) will hold in M' as a consequence of A[Z].
Moreover, none of a,...,n are in the extension of S (in M or
M') since only elements not in S are removed from the extension
of P in M'. Thus some Z(k) holds in M' while P(k) does not,
nor does S(k). This violates the condition that Z/S(x) -->
P(x) in M. <>
Theorem 1: A[P] |P/S-- B implies A[P] |P/S== B for any formula B.
Proof: Assume the hypothesis. Then any P/S-minimal model M of A[P] is
a model not only of A[P] but also of all the C[Z] in the
schema. But A[P] + {C[Z]} |-- B, so by the usual
completeness theorem of first-order logic, we are done. <>
Unfortunately the converse does not hold, as shown by Davis
[1980]. Let A[=] be Peano arithmetic (with or without the induction
postulate; here '=' is a binary predicate symbol). Then the minimal
models are isomorphic to the natural numbers; but no recursive
first-order theory, including one of the form A[=] + {C[Z]}, has as its
theorems precisely those sentences true of the natural numbers.
However, we shall show that a restricted converse does hold,
which seems more useful than one given by Davis. Namely, we show that
if a theory A[P] has a finite Herbrand universe (no function letters),
then the converse holds: if B holds in all (P/S-)minimal models of
A[P] then B is a theorem by circumscription of P in A[P]. This we then
generalize to certain cases with function letters. In the sequel we
shall assume A[P] to have a finite Herbrand universe unless otherwise
specified; let us call this assumption FHU (finite Herbrand universe),
which we will append to 'Lemma' or 'Theorem' to indicate such an
hypothesis. We first prove our results for ordinary (unprotected)
circumscription, and then observe that the proofs carry over for our
version as well.
We will proceed by induction on the number of quantifiers and
connectives in B. It will turn out that negation is the only difficult
case, and then only when applied to a single atom P(a). We will
attempt to use Z(x) as x=/=a in the complementary form x=c1 v x=c2 v
... v x=ck where the cj are all the Herbrand constants other than a.
This is where our assumption of finiteness comes in. In fact the
actual situation will be slightly more complicated, but suggested by
these comments.
Lemma 3: (FHU) If A[P] |c== P(a) then A[P] |-- P(a)
Proof: If P(a) is true in all minimal models of A[P] then since any
model M of A[P] has a minimal submodel N (recall the finite
Herbrand universe assumption) we have N |== P(a) and thus M |==
P(a): N can differ from M only in having possibly fewer P's,
never new ones. Finally, by completeness of first order logic,
A[P] |-- P(a).
Lemma 4: (FHU) If A[P] |c== (x)P(x) then A[P] |-- (x)P(x)
Proof: Same as for Lemma 3.
Lemma 5: (FHU) If A[P] |c== -P(a) then A[P] |c-- -P(a)
Proof: We will define a variation on disjunctive normal form: we say
F is a P-DNF formula if it is a (possibly universally
quantified) disjunction whose disjuncts are conjuncts of either
literals P(t) or -P(t) or subformulas Q not containing P.
Clearly any formula is equivalent to a P-DNF formula: we
Skolemize existential quantifiers in the prenex form and then
change CNF to DNF in the standard manner.
Let F be a P-DNF formula equivalent to A[P]. (Note for later
use that at least one of the Q's must hold if A[P] does.) Let
F' be the formula resulting from F by eliminating any disjuncts
that subsume other disjuncts, i.e., if D1 and D2 are disjuncts
of F and D1 --> D2, then remove D1. Note that F' is equivalent
to F and to A[P].
We show first that each disjunct Dc of F', say
P(c1)&...&P(ck)&-P(c'1)&...&-P(c'j)&Qc, determines a minimal
model of A[P]. For let M be the structure for A[P] with true
atoms P(c1),...,P(ck) as well as those entailed by Qc. Then M
is a model of A[P], and M is minimal since if any P(ci) could
be removed from M and still leave a model, then the disjunct Dc
would subsume another: each model must satisfy some disjunct.
(This shows that conversely every minimal model corresponds to
a disjunct. As a consequence, there are only a finite number
of minimal submodels of any model M of A[P]--viewed as sets of
true atoms--though possibly an infinite number of models M.)
Now if P(a) appears as a conjunct in any disjunct of F' then
P(a) will be true in some minimal model by the above argument.
So we conclude that P(a) does not so appear, assuming the
hypothesis of our Lemma, ie that -P(a) holds in each minimal
model of A[P].
To finish the proof we will show that P(a) cannot hold in any
model of A[P] + {C(Z)}. We will find formulas which will serve
for use in circumscribing P and will lead to the conclusion
-P(a). Again consider F' as before. For each disjunct Dc, ie,
P(c1)&...P(ck)&-P(c'1)&...&-P(c'j)&Qc
form
Zc(x): x=c1 v ... v x=ck .
The formulas Zc(x) will be our candidates for circumscription
of P in A[P]. Let us call the set of terms ci that appear in
any of the Zc(x) the P-requirement of A[P], or P-REQ for short.
Note that given Dc, the term a is provably distinct from
the terms c1 to ck since ci=/=a holds in each minimal model
of A[P] (otherwise since P(ci), then P(a) would hold there) and
thus also ci=/=a in each model of A[P]. (Actually, if P(x) is
the predicate x=/=a, then this argument is inadequate, but then
P(ci) gives ci=/=a directly.)
We first observe that each disjunct Dc(x) of F entails that for
the corresponding disjunct Zc(x), Zc(x) --> P(x). This is
because for all the terms ci in Zc(x), P(ci) is already a
conjunct of Dc(x): that is how we got Zc(x) in the first
place. So then we have that F (and therefore A[P]) entails the
disjunction of the formulas
Zc(x) --> P(x),
and specifically Dc entails Zc(x) --> P(x).
Now we observe that at least one of the A[Zc] holds given A[P].
Specifically, each disjunst Dc of A[P] entails A[Zc]. To show
this, first note that the P-DNF formula F, when all occurrences
of P are replaced by Zc, yields a result equivalent to A[Zc]
and also each disjunct Dc in F, i.e., P(c1)&...&P(ck) &
-P(c'1)&...&-P(c'j) & Qc, is thereby replaced by
[c1=c1 v ... v c1=ck] & ... & [ck=c1 v ... v ck=ck]
&
[c'1=/=c1 & ...& c'1=/=ck] & ... & [c'j=\=c1 & ... & c'j=\=ck]
&
Qc. (Note that each ci is in P-REQ.)
Now for any true disjunct Dc of F, Qc must be true. But then
the altered form of this disjunct as we have written just above
follows from Dc since none of the c'i's is in P-REQ (assuming
A[P] consistent), and Qc was already true. This shows that
A[Zc] holds if Dc does.
Now we have the ingredients for performing the circumscription
of P in A[P]. We know that at least one of the conditionals
Zc(x) --> P(x)
holds, as well as one of A[Zc], and in fact any Dc entails both
of these. Since one of the Dc holds (F is their disjunction)
then for some c we get both A[Zc] and Zc(x) --> P(x). This is
all we need for circumscription, and the conclusion is that
P(x) --> Zc(x) for some c, i.e., in each model M of A[P] there
will be a true Dc, and also P(x)-->Zc(x) holds there. Further,
a=/=ci in such M, since Dc entails P(ci) for each i, yet since
-P(a) holds in a minimal submodel N of M, then also -P(a) in M.
Since a is not among c1,...,ck then Zc(x) clearly forces x to
be distinct from a:
[x=c1 v ... v x=ck] & [x=/=c'1 & ... & x=/=c'j] & Qc.
Therefore P(x) forces x=/=a also, and the proof is complete. <>
Now we can establish our first completeness theorem:
Theorem 2: If A[P] has a finite Herbrand base, then for all
sentences B, A[P] |c== B iff A[P] |c-- B.
Proof: The left-to-right order of entailment we have already shown in
Theorem 1. Let us proceed to the converse.
By Lemma 4 above, the converse is true when B is an atom P(a)
or the formula (x)P(x). If B is instead -P(a) then by Lemma 5
again the converse is true. If B is some other formula having
one or fewer connectives, then it must not contain the letter
P. So again the converse is true since B will then hold not
only in minimal models but also in all models.
This shows that any sentence B with one or fewer connectives
and quantifiers satisfies the theorem. We proceed by induction
on the number of connectives and quantifiers in B. Assume the
theorem holds for all sentences with n or fewer connectives and
quantifiers. Let B have n+1 connectives and quantifiers. Then
B is of one of the forms
1) C v D
2) C & D
3) C --> D
4) -C
5) (x)C(x)
Now we may assume that v and - are being used as primitive
connectives which serve to define & and -->. Thus we work only
with v, -, and (x). Furthermore, we may assume B is written as
a P-DNF formula so that the case of -C arises only when C is
either P(a) or does not contain P.
Let M be a model of A[P]+{C(Z)}, and N a minimal submodel of M
(guaranteed to exist by the finite Herbrand base). We will
show that if B holds in N then it also holds in M, thereby
establishing the theorem.
If then B is of the form C v D, since C and D will have fewer
than n connectives we may apply the inductive assumption to
conclude that either C or D holds in M, since either C or D
will hold in N.
If B is of the form -C, then either C is of the form P(a) or
does not contain P, and in each case we already know -C holds
in M.
Finally, if B is of the form (x)C(x), then since M and N have
the same domain, we have C(d) holds in N for each d in M, and
therefore also C(d) holds in M by inductive assumption.
With this we are done. <>
This proof provides the justification for our earlier claim
that the only cases of significance for circumscription C[Z] are those
in which Z is a disjunction x=c1 v ... v x=ck. That is, no further
circumscribing will lead to new information. As a consequence we will
have new characterizations of circumscription over theories with finite
Herbrand universes, and, we anticipate, even infinite universes in
certain cases. Reiter [1982] addresses the problem of selecting
appropriate formulas Z, in his work relating circumscription and the
closed world assumption using ideas in Clark [1978]. Here we have
delimited precisely the class of Z's that are useful in general in the
FHU case. McCarthy [1980] uses two examples to illustrate
circumscription and chooses judiciously a disjunction in one and
multiple cases for Z in the other; we have used exactly these
situations to show that all circumscriptive theorems are obtainable
this way, indicating that no further ingenuity is needed in
constructing Z's in such cases. The P-DNF version of A[P] determines
the minimal models and hence the theorems, in analogy with the work of
Reiter and Clark but for arbitrary formulas (not just Horne clauses)
and allowing for possible protected data.
Let us note finally that the above result also holds for the
protected form of circumscription, giving us the following:
Theorem 3: If A[P] has a finite Herbrand base, then for all
sentences B, A[P] |P/S== B iff A[P] |P/S-- B.
Proof: We simply use the same proofs as in the above Lemmas and Theorem
in which it is easily seen that the addition of the 'protection
clause' S(x) in no way affects the arguments, except possibly
in the very last line of the proof of Theorem 2, namely, that
'P(x) forces x=/=a'. We should have here 'P(x) & -S(x) forces
x=/=a,' and then the only new case to handle is that in which
a itself is protected: S(a). But then P/S-minimal models N of M
will have to agree with M on P(a), so automatically we get P(a)
to fail in all models. <>
It is instructive to consider the following example: Let A[P]
consist of the data P(a), -P(b) v -P(c). Then there are three models
of A[P]:
1. {P(a)}
2. {P(a), P(b)}
3. {P(a), P(c)}
Of these, only 1 is minimal, and so the formulas true in 1 are the
circumscriptive theorems of A[P], for all choices of Z at once! Notice
that the theory A'[P] having ONLY P(a) as axiom also has these three
models as well as: 4. {P(a), P(b), P(c)} which still is not minimal.
So A and A' have the same minimal models and hence the same
circumscriptive theorems. In fact in both theories we have the
theorems -P(b) and -P(c), so that the axiom -P(b) v -P(c) in A is
circumscriptively redundant.
Now suppose we wish to protect b and c in A so that ALL we know
about P(b) and P(c) is that they are not jointly true, i.e., -P(b) v
-P(c) represents real uncertainty. Then we find that 1, 2, and 3 are
the only models and all are minimal. Furthermore, although -P(b) v
-P(c) holds in each, neither -P(b) nor -P(c) does, so that the
protection has really worked. But now if we pass to A' and protect b
and c, we find still all four models as before and all are minimal, so
that not even -P(b) v -P(c) holds.
Although the completeness result has shown us what the theorems
of these four theories are, we see from this example that negative data
(-P(b) v -P(c)) can have a non-redundant effect when there are
protected constants. This shows a strong distinction with the situation
in Lemma 1 for ordinary circumscription.
←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←
We think that these results may generalize to certain cases of
infinite Herbrand bases, and we have tentative conjectures on what such
cases might be.
------------------------------------------------------------------------------
Acknowledgements
Our work obviously depends greatly on that of John McCarthy. We have
also been influenced by work of and discussions with Ray Reiter.
This paper was written with support from the following grants:
AFOSR-82-0303, for J. Minker and D. Perlis
NSFD MCS 79 19418, for J. Minker
Summer Research Award, Univ. of Md. General Research Board, for D. Perlis
Bibliography
Clark, K. Negation as failure, in Logic and Databases, Gallaire and
Minker (eds) (pp 293-322). Plenum Press, NY 1978.
Davis, M. The mathematics of non-monotonic reasoning. Artificial
Intelligence 13, (pp 73-80), 1980.
McCarthy, J. Circumscription--A form of non-monotonic
reasoning. Artificial Intelligence 13 (pp 27-39), 1980.
Minker, J. On theories of definite and indefinite databases.
Tech. Report. Univ. of Maryland
Minker, J. On indefinite databases and the closed-world assumption.
Springer-Verlag Lecture Notes in Computer Science, v.138, pp
292-308. Sixth Conference on Automated Deduction. New
York, NY. 1982.
Reiter, R. A logic for default reasoning. Artificial Intelligence
13 (pp 81-132), 1980.
Reiter, R. On closed world databases. In Logic and Data Bases.
(pp55-76) Gallaire and Minker (eds.) Plenum, 1978.
Reiter, R. Circumscription implies predicate completion
(sometimes). Proceedings of AAAI-82. (pp418-420)